\begin{tabbing}
$\forall$${\it tg}$:Id, $k$:Knd, $l$:IdLnk, $T$, $B$:Type, $f$:($B$$\rightarrow$($T$ List)).
\\[0ex](rcv($l$,${\it tg}$) $=$ $k$ $\Rightarrow$ $T$ $=$ $B$)
\\[0ex]$\Rightarrow$ \=@source($l$): ma{-}single{-}sends0($B$;$T$;$k$;$l$;${\it tg}$;$f$) $\in$ Dsys\+
\\[0ex]\& (\=$\forall$$D$:Dsys.\+
\\[0ex]@source($l$): ma{-}single{-}sends0($B$;$T$;$k$;$l$;${\it tg}$;$f$) $\subseteq$ $D$
\\[0ex]$\Rightarrow$ \=$D$ \+
\\[0ex]realizes ${\it es}$.
\\[0ex]($\forall$$e$:E. loc($e$) $=$ source($l$) $\in$ Id $\Rightarrow$ kind($e$) $=$ $k$ $\in$ Knd $\Rightarrow$ valtype($e$) $\subseteq\rho$ $B$)
\\[0ex]\& ($\forall$$e$:E. kind($e$) $=$ rcv($l$,${\it tg}$) $\in$ Knd $\Rightarrow$ valtype($e$) $\subseteq\rho$ $T$)
\\[0ex]\& (\=$\forall$$e$:E.\+
\\[0ex]loc($e$) $=$ source($l$) $\in$ Id
\\[0ex]$\Rightarrow$ kind($e$) $=$ $k$ $\in$ Knd
\\[0ex]$\Rightarrow$ (\=$\exists$$L$:\{${\it e'}$:E$\mid$ kind(${\it e'}$) $=$ rcv($l$,${\it tg}$) $\in$ Knd \} List.\+
\\[0ex]($\forall$${\it e'}$:E. (${\it e'}$ $\in$ $L$) $\Leftrightarrow$ kind(${\it e'}$) $=$ rcv($l$,${\it tg}$) $\in$ Knd \& sender(${\it e'}$) $=$ $e$ $\in$ E)
\\[0ex]\& ($\forall$$e_{1}$, $e_{2}$:E. $e_{1}$ before $e_{2}$ $\in$ $L$ $\Rightarrow$ ($e_{1}$ $<$loc $e_{2}$))
\\[0ex]\& map($\lambda$${\it e'}$.val(${\it e'}$);$L$) $=$ $f$(val($e$)) $\in$ $T$ List)))
\-\-\-\-\-
\end{tabbing}